//this is the precondition for sum
/*@ n>=0
 */
int sum (int n)
{
  int s, i;
  i=0;
  s=0;
  while(i<=n) /*@ (s * 2==(i-1)*i) && (i<=n+1) */
  {
    s=s+i;
    i=i+1;
  }
  return s;
}
/*@  result * 2 == n*(n+1)
 */
//this is the post-condition for sum


//default value is true
/*@ */
void main()
{
  int x;
  x = sum (100);
  print(x);
  return;
}
/*@ */
//default value is true